-
Notifications
You must be signed in to change notification settings - Fork 138
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Filling Cubes in a Few Lines of Code #1053
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks very nice! I did not see it before
Can you show some examples where to use this in the library?
tp i = transport-filler (λ i → X i) a i | ||
|
||
bottom : (i : I) → X i | ||
bottom i = pd (x i0 1=1) (x i1 1=1) i |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is also https://github.com/agda/cubical/blob/master/Cubical/Foundations/Path.agda#L130 which might be the next dimension, but I did not think hard about it...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's exactly extend₁
with ϕ = j ∨ ~ j
. But it seems a bit hard to generalize this argument to higher dimensions...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Can you use https://github.com/agda/cubical/blob/master/Cubical/Foundations/Prelude.agda#L548 here?
Ok.
Added an example at the end of the file. The main application I came up with is the same as in #910. I believe this new approach is better. It's simpler and the inductive pattern is very clear. However, I'm unsure if Agda's meta-programming could handle partial elements and (non-fibrant) extension types that needed. But since these operations are more general than just cube-filling (they allow for an arbitrary cofibration Btw, I also think the cube-filling results in library need reorganization. They are separated in several files like here, here and here. Maybe they would be better put together and deduced as consequences of these |
Yeah, reorganizing them a bit sounds very reasonable. Feel free to do it in a future PR! I'm happy with this one now so will merge |
* done * fix Everything * update * add an example * fix * typos * alignment
I haven't worked on the cube-filling stuff in quite some time. However, I recently discovered a surprisingly easy way to do the same job with just a few lines of code. In fact the result seems to be more powerful than the previous one. I've written a short note about this, which you can find here.
I'm curious whether or not someone in the cubical type theory community has found this before, since it is so simple...